1. Field of the Invention
The present invention relates to a pre-condition generation device, a post-condition generation device, and a method for generating a pre-condition and a post-condition of a computer program described by using an imperative programming language.
2. Related Art
As a fundamental method for representing specifications and properties of a program described in an imperative programming language, a set of a pre-condition and a post-condition of the program is widely used. Known as a background theory of the method is an axiomatic semantics, which is a methodology showing the validity of the program by deriving the pre-condition and the post-condition of the program based on an axiom and an inference rule. Hoare's logic is known as a concrete example of the axiomatic semantics.
JP-A 2005-182806 (Kokai) discloses a method for generating a program satisfying specifications described based on the axiomatic semantics, for example.
When performing verification etc. of the program by using the above-mentioned axiomatic semantics, every part of the program is not always given with the pre-condition and the post-condition. In such a case, it is desirable to calculate a weakest pre-condition and a strongest post-condition by using the information before and after each part of the program (the weakest pre-condition and the strongest post-condition are obtained through propagation). For example, when the assignment statement of “x:=x+1;” is given with the post-condition of “x>10,” the weakest pre-condition of the assignment statement becomes “x>9.” However, it is not always easy to automatically calculate the weakest pre-condition and the strongest post-condition.
This is because, for example, when the program has a loop therein, it is required to automatically derive a loop invariant which is always satisfied before and after the loop is executed, but it is not decidable (in an imperative programming language generally used) (A. Blass and Y. Gurevich. Inadequacy of Computable Loop Invariants. ACM Transactions on Computational Logic. 2 (1): 1-11, January 2001.).
The method for automatically estimating the loop invariant has been studied (for example, N. Suzuki, and K. Ishihata. Implementation of an Array Bound Checker. 4th ACM Symposium on Principles of Programming Languages. Los Angeles, Calif. (January 1977).) However, such a method is not widely used because of the problems in terms of computational complexity and limited applicability.